Nuprl Lemma : nat_ind_a
13,42
postcript
pdf
P
:(
{k}).
P
(0)
(
i
:
.
P
(
i
- 1)
P
(
i
))
{
i
:
.
P
(
i
)}
latex
Up
int
1
,
int
1
Definitions
False
,
A
,
A
B
,
t
T
,
{
T
}
,
x
(
s
)
,
P
Q
,
,
,
x
:
A
.
B
(
x
)
,
i
j
,
,
S
T
Lemmas
nat
plus
inc
,
le
wf
,
nat
plus
wf
,
nat
wf
,
ge
wf
,
nat
properties
origin
P:(
{k}). P(0) 
(i:
. P(i - 1) P(i)) {i:. P(i)} P:({k}). P(0) (i:. P(i - 1) P(i)) {i:. P(i)} 
A
B
T Qx:A. B(x)
j 
T